Formal Methods for Adaptive Control of Dynamical Systems

摘要

We develop a method to control discrete-time systems with constant butinitially unknown parameters from linear temporal logic (LTL) specifications.We introduce the notions of (non-deterministic) parametric and adaptivetransition systems and show how to use tools from formal methods to computeadaptive control strategies for finite systems. For infinite systems, we firstcompute abstractions in the form of parametric finite quotient transitionsystems and then apply the techniques for finite systems. Unlike traditionaladaptive control methods, our approach is correct by design, does not require areference model, and can deal with a much wider range of systems andspecifications. Illustrative case studies are included.